The Equivalence between Presburger Arithmetic and Its Cyclic Proof System
#PPL2023
要旨
Presburger算術と循環Pressburger算術の証明能力は同じ．
$ \mathbf{P}_+ = \mathbf{CP}^\omega_+
以下似た内容だったので帰納法に関する推論の計算複雑性の内容も含む
証明体系
$ \mathbf{LKID}
$ \mathbf{LK}に通常の帰納法を推論規則として形式化したものを追加
$ \mathbf{LKID}^\omega
$ \mathbf{LK}に無限降下法による証明を形式化したものを追加
導出木のサイズが無限でも良い
ただし大域トレース条件を満たす必要があり
これはBüchiオートマトンで判定可能
$ \mathbf{CLKID}^\omega
$ \mathbf{LKID}^\omegaの導出木が有限
証明能力
$ \mathbf{LKID} < \mathbf{CLKID}^\omega < \mathbf{LKID}^\omega
Berardi and Tatsuta. 2019 - Classical System of Martin-Löf’s Inductive Definitions is not Equivalent to Cyclic Proofs.
$ \mathbf{CLKID}^\omegaで証明可能だが$ \mathbf{LKID}では証明不能なシーケントが存在する
$ \mathbf{CLKIDω} + \mathbf{PA} =$ \mathbf{LKID}+ \mathbf{PA}
Berardi and Tatsuta. 2017 - Equivalence of inductive definitions and cyclic proofs under arithmetic.
$ \mathbf{CA} = \mathbf{PA}
循環算術$ \mathbf{CA}とPeano算術$ \mathbf{PA}の証明能力は同等
A. K. Simpson. 2017; "Cyclic Arithmetic Is Equivalent to Peano Arithmetic"
$ \mathbf{IΣ_n} < \mathbf{CΣ_n}
A. Das; 2020; "On the Logical Complexity of Cyclic Arithmetic"
Presburger算術
言語:$ \mathscr{L}_{P_+} := \lang =,\leq,s,+,0\rang
Peano算術の公理から乗算を切ったもの
完全な理論かつ計算可能$ \Delta_1
循環Pressburger算術の$ \mathbf{CP}^\omega_+
証明木全体が大域トレース条件を満たす必要がある
大域トレース条件を満たす木$ \mathbf{P}^\omega_+